Nuprl Lemma : atom-free-union
0,22
postcript
pdf
A
,
B
:Type. AtomFree(Type;
A
)
AtomFree(Type;
B
)
AtomFree(Type;
A
+
B
)
latex
Definitions
Type
,
t
T
,
x
:
A
.
B
(
x
)
,
AtomFree(
T
;
x
)
,
left
+
right
,
x
.
A
(
x
)
,
x
:
A
B
(
x
)
,
P
Q
Lemmas
atom-free
wf
origin
A, B:Type. AtomFree(Type;A) 
AtomFree(Type;B) AtomFree(Type;A+B) A, B:Type. AtomFree(Type;A) AtomFree(Type;B) AtomFree(Type;A+B) 
Tx:A. B(x)
x.A(x)
B(x) Q